//  /=============================================================/
//  |   Auteurs  : J.JULLIEN / R.HERLEMAN / R.CHAILAN             |
//  |   Fichier  : matrice.c                                      |
//  |   Date     : 10/04/2009                                     |
//  |   Objet    : Définition du type "t_MatriceCreuse" &         |
//  |              ses fonctions associées                        |
//  /=============================================================/

#include "matrice.h"

/* ------------------------------------------------------------------------ */
/* ---------------- Déclaration types et fonctions locales ---------------- */
/* ------------------------------------------------------------------------ */

char *tabEtat[10] = { "SATISFAITE", "FALSIFIEE", "INCHANGEE", "RACCOURCIE"} ;

typedef struct t_CoupleVarVal {
  int var;
  int val;
} t_CoupleVarVal;

/*----------------------------------------------------------------------------
Nom              : matriceInit
Prérequis        : -
Action           : Reserve l'espace necessaire et initialise les champs d'une
                   matrice creuse de nbClauses x nbVariables et la retourne.
Type de retour   : t_MatriceCreuse
Variable(s)      :  
  E   int   nbClauses - Nombre de clauses
  E   int   nbVariables - Nombre de variables
----------------------------------------------------------------------------*/
t_MatriceCreuse matriceInit (int nbClauses, int nbVariables);

/*----------------------------------------------------------------------------
Nom              : matriceGetValeurLitteral
Prérequis        : -
Action           : Retourne la valeur d'un litteral
Type de retour   : int
Variable(s)      :  
  E   t_MatriceCreuse   mC - L'ensemble des clauses
  E   T_Litteral        lit - Le litteral dont on veut la valeur
----------------------------------------------------------------------------*/
int matriceGetValeurLitteral (t_MatriceCreuse mC, t_Litteral lit);

/*----------------------------------------------------------------------------
Nom              : matriceSetVariable
Prérequis        : var existe
Action           : Affecte la variable var à la valeur val en mettant à jour
                   l'ensemble des variables d'états et compteurs
Type de retour   : -
Variable(s)      :  
  E/S t_MatriceCreuse*   mC - L'ensemble des clauses
  E   int                var - Numéro de la variable à affecter
  E   int                val - Valeur 1 ou 0, sinon neutre
----------------------------------------------------------------------------*/
void matriceSetVariable (t_MatriceCreuse *mC, int var, int val);

/*----------------------------------------------------------------------------
Nom              : matriceChoisirVariableValeur
Prérequis        : -
Action           : Choisi la variable et sa valeur afin d'optimiser
                   l'algorithme de résolution.
Stratégie        : On choisit la premiere variable neutre de la clause qui
                   contient le plus petit nombre de variables neutres.
Type de retour   : t_CoupleVarVal
Variable(s)      :  
  E   t_MatriceCreuse   mC - L'ensemble des clauses
----------------------------------------------------------------------------*/
t_CoupleVarVal matriceChoisirVariableValeur(t_MatriceCreuse mC);

/*----------------------------------------------------------------------------
Nom              : hashAjouter
Prérequis        : numClause existe
Action           : Ajoute la clause numClause à la table de hashage tout en
                   gardant à jour le minNbClauses et les pointeurs de la
                   clause
Type de retour   : -
Variable(s)      :  
  E/S t_MatriceCreuse*   mC - L'ensemble des clauses
  E   int                numClause - numéro de la clause à ajouter
----------------------------------------------------------------------------*/
void hashAjouter (t_MatriceCreuse* mC, int numClause);

/*----------------------------------------------------------------------------
Nom              : hashRetirer
Prérequis        : numClause existe
Action           : Retire la clause numClause de la table de hashage tout en
                   gardant à jour le minNbClauses et les pointeurs de la
                   clause
Type de retour   : -
Variable(s)      :  
  E/S t_MatriceCreuse*   mC - L'ensemble des clauses
  E   int                numClause - numéro de la clause à retirer
----------------------------------------------------------------------------*/
void hashRetirer(t_MatriceCreuse* mC, int numClause);

/* ------------------------------------------------------------------------ */
/* -------------------- Définition fonctions exportées -------------------- */
/* ------------------------------------------------------------------------ */

void matriceSetVariableAChoisir (t_MatriceCreuse *mC, int val) {
  mC->valeurAChoisir = val;
}

t_MatriceCreuse matriceCreerDepuisFichier(FILE * f){
  int nbClauses, nbVariables; 
  t_MatriceCreuse mC;
  
  fscanf(f, "%d%d\n", &nbVariables, &nbClauses);
  mC = matriceInit(nbClauses, nbVariables);
  
  mC.minNbNeutres = mC.nbVariables;
  
  int clause;
  int variable;
  char s;
  t_Litteral *el;
  
  for (clause = 0; clause < mC.nbClauses; clause++) {
    fscanf(f, "%c", &s);
    while (s != '\n' ) {
      fscanf(f, "%d", &variable);
      el = litteralInit(s, clause, variable - 1 );
      
      clauseAjouterLitteral(&mC.clauses[clause], el);
      variableAjouterLitteral(&mC.variables[el->variable], el);
      
      fscanf(f, "%c", &s);
      if (s == ',') {
        fscanf(f, "%c", &s);
      }
    }
    hashAjouter(&mC,clause);
    if (mC.minNbNeutres > mC.clauses[clause].nbNeutres
        && mC.clauses[clause].nbNeutres != 0) {
      mC.minNbNeutres = mC.clauses[clause].nbNeutres;
    }
  }
  fclose(f);
  
  return mC;
}

int matriceResolution (t_MatriceCreuse *mC) {
  if (matriceEstResolue(*mC)) {
    return 1;
  } else {
    if (mC->nbFalsifiees > 0) {
      return 0;
    } else {
      t_CoupleVarVal c = matriceChoisirVariableValeur(*mC);
      matriceSetVariable (mC,c.var,c.val);
      if (matriceResolution (mC)) {
        return 1;
      } else {
        matriceSetVariable (mC,c.var,1-(c.val));
        if (matriceResolution(mC)) {
          return 1;
        } else {
          matriceSetVariable (mC,c.var,-1);
          return 0;
        }
      }
    }
  }
}

int matriceEstResolue (t_MatriceCreuse mC) {
  return mC.nbSatisfaites == mC.nbClauses;
}

int matriceVerifierAffectation(t_MatriceCreuse mC, FILE* f) {
  int i;
  t_MatriceCreuse mC2 = matriceCreerDepuisFichier(f);
  
  for (i = 0; i<mC.nbVariables; i++) {
    matriceSetVariable (&mC2,i,variableGetValeur(mC.variables[i]));
  }
  
  return matriceEstResolue(mC2);
}

void matriceAfficherMatrice(t_MatriceCreuse mC) {
  int i;
  printf("  | ");
  for (i = 0; i<mC.nbVariables; i++) {
    printf("%d ", i+1);
  }
  
  printf("\n--|-");
  for (i = 0; i<mC.nbVariables; i++) {
    printf("--");
  }
  printf("\n");
  
  for (i = 0; i<mC.nbClauses; i++) {
    clauseAfficherLigne(mC.clauses[i]);
    printf("\n");
  }
}

void matriceAfficherEnsemble(t_MatriceCreuse mC) {
  int i;
  
  printf("{"); 
  for (i = 0; i<mC.nbClauses; i++) {
    clauseAfficherEnsemble(mC.clauses[i]);
    if (i+1 != mC.nbClauses) {
      printf(", ");
    }    
  }
  printf("}\n");
}

void matriceAfficherFormule(t_MatriceCreuse mC) {  
  int i;
 
  for (i = 0; i<mC.nbClauses; i++) {
    clauseAfficherFormule(mC.clauses[i]);
    if (i+1 != mC.nbClauses) {
      printf(" ∧ ");
    }
  }
  printf("\n");
}

void matriceAfficherDebug (t_MatriceCreuse mC) {
  
  printf("CLAUSES (%d) :\n", mC.nbClauses);
  printf("• NbSatisfaites : %d\n", mC.nbSatisfaites);
  printf("• NbFalsifiees  : %d\n", mC.nbFalsifiees);
  printf("• NbInchangées  : %d\n", mC.nbInchangees);
  printf("• NbRaccourcies : %d\n\n", mC.nbRaccourcies);
  
  int i;
  for (i = 0; i<mC.nbClauses; i++) {
    clauseAfficherDebug(mC.clauses[i]);
  }
  
  printf("\n\nVARIABLES (%d) :\n", mC.nbVariables);
  for (i = 0; i<mC.nbVariables; i++) {
    variableAfficherDebug(mC.variables[i]);
  }

}

void matriceAfficherSimplifiee (t_MatriceCreuse mC) {
  int i;
  printf("{"); 
  for (i = 0; i<mC.nbClauses; i++) {
    if (mC.clauses[i].etat != SATISFAITE) {
      t_Litteral *c = clauseGetLitteral(mC.clauses[i]);
      printf("{");
      while (c != NULL) {
        if (matriceGetValeurLitteral(mC, *c) != 0
            && matriceGetValeurLitteral(mC, *c) != 1) {
          printf(" ");
          litteralAfficherPredicat(*c);
          printf(" ");
        }
        c = (*c).variableSuiv;
      }
      printf("}");
    }
  }
  printf("}\n");
}

void matriceAfficherValeurs (t_MatriceCreuse mC) {
  int i;
  for (i = 0; i<mC.nbVariables; i++) {
    variableAfficherValeur(mC.variables[i]);
  }
}

/* ------------------------------------------------------------------------ */
/* -------------------- Définition fonctions locales ---------------------- */
/* ------------------------------------------------------------------------ */

t_MatriceCreuse matriceInit(int nbClauses, int nbVariables){
  t_MatriceCreuse mC;
 
  mC.clauses = (t_Clause*) malloc(nbClauses * sizeof(t_Clause));
  mC.variables = (t_Variable*) malloc(nbVariables * sizeof(t_Variable));
  mC.hashClauses = (t_Clause**) malloc((nbVariables+1) * sizeof(t_Clause*));

  mC.nbClauses = nbClauses;
  mC.nbVariables = nbVariables;
  
  mC.nbInchangees = mC.nbClauses;
  mC.nbSatisfaites = 0;
  mC.nbFalsifiees = 0;
  mC.nbRaccourcies = 0;

  int i;
  for (i = 0; i < mC.nbClauses; i++) {
    mC.clauses[i] = clauseInit(i);
  }
  
  for (i = 0; i < mC.nbVariables; i++) {
    mC.variables[i] = variableInit(i);
    mC.hashClauses[i] = NULL;
  }
  
  return mC;
}

int matriceGetValeurLitteral (t_MatriceCreuse mC, t_Litteral lit) {
  return litteralGetValeur(lit,variableGetValeur(mC.variables[lit.variable]));
}

void matriceSetVariable (t_MatriceCreuse *mC, int var, int val) {
  t_Etat eInitial;
  t_Litteral *l = variableGetLitteral(mC->variables[var]);
  //printf("Affectation de %d à %d\n", var, val);
  while (l != NULL) {
    variableMAJCompteurs(&mC->variables[var], *l, val);
    eInitial = mC->clauses[l->clause].etat;
    switch (eInitial) {
      case SATISFAITE : mC->nbSatisfaites--; break;
      case FALSIFIEE : mC->nbFalsifiees--; break;
      case RACCOURCIE : mC->nbRaccourcies--; break;
      case INCHANGEE : mC->nbInchangees--; break;
    }
    hashRetirer(mC, l->clause);
    clauseMAJCompteurs(&mC->clauses[l->clause], *l,
                       variableGetValeur(mC->variables[var]), val);
    hashAjouter(mC, l->clause);
    switch (mC->clauses[l->clause].etat) {
      case SATISFAITE : mC->nbSatisfaites++; break;
      case FALSIFIEE : mC->nbFalsifiees++; break;
      case RACCOURCIE : mC->nbRaccourcies++; break;
      case INCHANGEE : mC->nbInchangees++; break;
    }
    //printf("  Clause %d passe de %s à %s\n", l->clause,
    //      tabEtat[eInitial], tabEtat[mC->clauses[l->clause].etat]);
    l = l->clauseSuiv;
  } 
  //printf("\n");
  variableSetValeur (&mC->variables[var], val);
}

t_CoupleVarVal matriceChoisirVariableValeur(t_MatriceCreuse mC) {
  t_CoupleVarVal c;
  t_Litteral *l = mC.hashClauses[mC.minNbNeutres]->litteral;
  while (l != NULL && matriceGetValeurLitteral(mC, *l) != -1) {
    l = l->variableSuiv;
  }
  c.var = l->variable;
  c.val = mC.valeurAChoisir;
  return c;
}

void hashRetirer (t_MatriceCreuse* mC, int numClause) {
  int place;
  if (mC->clauses[numClause].etat == SATISFAITE) {
    place = 0;
  } else {
    place = mC->clauses[numClause].nbNeutres;
  }
  
  if (mC->clauses[numClause].hashPred != NULL) {
    mC->clauses[numClause].hashPred->hashSuiv=mC->clauses[numClause].hashSuiv;
  } else {
    mC->hashClauses[place] = mC->clauses[numClause].hashSuiv;
  }
    
  if (mC->clauses[numClause].hashSuiv != NULL) {
    mC->clauses[numClause].hashSuiv->hashPred=mC->clauses[numClause].hashPred;
  }
  mC->clauses[numClause].hashPred = NULL;
  mC->clauses[numClause].hashSuiv = NULL;
  
  if (mC->clauses[numClause].nbNeutres == mC->minNbNeutres
      && mC->hashClauses[mC->clauses[numClause].nbNeutres] == NULL) {
    int i = mC->clauses[numClause].nbNeutres;
    while (i<mC->nbVariables && mC->hashClauses[i] == NULL) {
      i++;
    }
    mC->minNbNeutres = i;
  }
}

void hashAjouter (t_MatriceCreuse* mC, int numClause) {
  int place;
  if (mC->clauses[numClause].etat == SATISFAITE) {
    place = 0;
  } else {
    place = mC->clauses[numClause].nbNeutres;
  }
  mC->clauses[numClause].hashSuiv = mC->hashClauses[place];
  mC->hashClauses[place]= &mC->clauses[numClause];
  mC->clauses[numClause].hashPred = NULL;
  if (mC->clauses[numClause].hashSuiv != NULL) {
    mC->clauses[numClause].hashSuiv->hashPred = &mC->clauses[numClause];
  }
  
  if (mC->clauses[numClause].etat != SATISFAITE
      && mC->clauses[numClause].nbNeutres != 0
      && mC->clauses[numClause].nbNeutres < mC->minNbNeutres) {
    mC->minNbNeutres = mC->clauses[numClause].nbNeutres;
  }
}
